Termination w.r.t. Q of the following Term Rewriting System could not be shown:
Q restricted rewrite system:
The TRS R consists of the following rules:
top1(free1(x)) -> top1(check1(new1(x)))
new1(free1(x)) -> free1(new1(x))
old1(free1(x)) -> free1(old1(x))
new1(serve) -> free1(serve)
old1(serve) -> free1(serve)
check1(free1(x)) -> free1(check1(x))
check1(new1(x)) -> new1(check1(x))
check1(old1(x)) -> old1(check1(x))
check1(old1(x)) -> old1(x)
Q is empty.
↳ QTRS
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
top1(free1(x)) -> top1(check1(new1(x)))
new1(free1(x)) -> free1(new1(x))
old1(free1(x)) -> free1(old1(x))
new1(serve) -> free1(serve)
old1(serve) -> free1(serve)
check1(free1(x)) -> free1(check1(x))
check1(new1(x)) -> new1(check1(x))
check1(old1(x)) -> old1(check1(x))
check1(old1(x)) -> old1(x)
Q is empty.
Q DP problem:
The TRS P consists of the following rules:
OLD1(free1(x)) -> OLD1(x)
CHECK1(new1(x)) -> CHECK1(x)
TOP1(free1(x)) -> TOP1(check1(new1(x)))
NEW1(free1(x)) -> NEW1(x)
CHECK1(old1(x)) -> CHECK1(x)
CHECK1(new1(x)) -> NEW1(check1(x))
TOP1(free1(x)) -> CHECK1(new1(x))
CHECK1(free1(x)) -> CHECK1(x)
TOP1(free1(x)) -> NEW1(x)
CHECK1(old1(x)) -> OLD1(check1(x))
The TRS R consists of the following rules:
top1(free1(x)) -> top1(check1(new1(x)))
new1(free1(x)) -> free1(new1(x))
old1(free1(x)) -> free1(old1(x))
new1(serve) -> free1(serve)
old1(serve) -> free1(serve)
check1(free1(x)) -> free1(check1(x))
check1(new1(x)) -> new1(check1(x))
check1(old1(x)) -> old1(check1(x))
check1(old1(x)) -> old1(x)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
OLD1(free1(x)) -> OLD1(x)
CHECK1(new1(x)) -> CHECK1(x)
TOP1(free1(x)) -> TOP1(check1(new1(x)))
NEW1(free1(x)) -> NEW1(x)
CHECK1(old1(x)) -> CHECK1(x)
CHECK1(new1(x)) -> NEW1(check1(x))
TOP1(free1(x)) -> CHECK1(new1(x))
CHECK1(free1(x)) -> CHECK1(x)
TOP1(free1(x)) -> NEW1(x)
CHECK1(old1(x)) -> OLD1(check1(x))
The TRS R consists of the following rules:
top1(free1(x)) -> top1(check1(new1(x)))
new1(free1(x)) -> free1(new1(x))
old1(free1(x)) -> free1(old1(x))
new1(serve) -> free1(serve)
old1(serve) -> free1(serve)
check1(free1(x)) -> free1(check1(x))
check1(new1(x)) -> new1(check1(x))
check1(old1(x)) -> old1(check1(x))
check1(old1(x)) -> old1(x)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 4 SCCs with 4 less nodes.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
OLD1(free1(x)) -> OLD1(x)
The TRS R consists of the following rules:
top1(free1(x)) -> top1(check1(new1(x)))
new1(free1(x)) -> free1(new1(x))
old1(free1(x)) -> free1(old1(x))
new1(serve) -> free1(serve)
old1(serve) -> free1(serve)
check1(free1(x)) -> free1(check1(x))
check1(new1(x)) -> new1(check1(x))
check1(old1(x)) -> old1(check1(x))
check1(old1(x)) -> old1(x)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.
OLD1(free1(x)) -> OLD1(x)
Used argument filtering: OLD1(x1) = x1
free1(x1) = free1(x1)
Used ordering: Precedence:
trivial
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
P is empty.
The TRS R consists of the following rules:
top1(free1(x)) -> top1(check1(new1(x)))
new1(free1(x)) -> free1(new1(x))
old1(free1(x)) -> free1(old1(x))
new1(serve) -> free1(serve)
old1(serve) -> free1(serve)
check1(free1(x)) -> free1(check1(x))
check1(new1(x)) -> new1(check1(x))
check1(old1(x)) -> old1(check1(x))
check1(old1(x)) -> old1(x)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
NEW1(free1(x)) -> NEW1(x)
The TRS R consists of the following rules:
top1(free1(x)) -> top1(check1(new1(x)))
new1(free1(x)) -> free1(new1(x))
old1(free1(x)) -> free1(old1(x))
new1(serve) -> free1(serve)
old1(serve) -> free1(serve)
check1(free1(x)) -> free1(check1(x))
check1(new1(x)) -> new1(check1(x))
check1(old1(x)) -> old1(check1(x))
check1(old1(x)) -> old1(x)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.
NEW1(free1(x)) -> NEW1(x)
Used argument filtering: NEW1(x1) = x1
free1(x1) = free1(x1)
Used ordering: Precedence:
trivial
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
Q DP problem:
P is empty.
The TRS R consists of the following rules:
top1(free1(x)) -> top1(check1(new1(x)))
new1(free1(x)) -> free1(new1(x))
old1(free1(x)) -> free1(old1(x))
new1(serve) -> free1(serve)
old1(serve) -> free1(serve)
check1(free1(x)) -> free1(check1(x))
check1(new1(x)) -> new1(check1(x))
check1(old1(x)) -> old1(check1(x))
check1(old1(x)) -> old1(x)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
CHECK1(new1(x)) -> CHECK1(x)
CHECK1(old1(x)) -> CHECK1(x)
CHECK1(free1(x)) -> CHECK1(x)
The TRS R consists of the following rules:
top1(free1(x)) -> top1(check1(new1(x)))
new1(free1(x)) -> free1(new1(x))
old1(free1(x)) -> free1(old1(x))
new1(serve) -> free1(serve)
old1(serve) -> free1(serve)
check1(free1(x)) -> free1(check1(x))
check1(new1(x)) -> new1(check1(x))
check1(old1(x)) -> old1(check1(x))
check1(old1(x)) -> old1(x)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.
CHECK1(free1(x)) -> CHECK1(x)
Used argument filtering: CHECK1(x1) = x1
new1(x1) = x1
old1(x1) = x1
free1(x1) = free1(x1)
Used ordering: Precedence:
trivial
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
CHECK1(new1(x)) -> CHECK1(x)
CHECK1(old1(x)) -> CHECK1(x)
The TRS R consists of the following rules:
top1(free1(x)) -> top1(check1(new1(x)))
new1(free1(x)) -> free1(new1(x))
old1(free1(x)) -> free1(old1(x))
new1(serve) -> free1(serve)
old1(serve) -> free1(serve)
check1(free1(x)) -> free1(check1(x))
check1(new1(x)) -> new1(check1(x))
check1(old1(x)) -> old1(check1(x))
check1(old1(x)) -> old1(x)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.
CHECK1(old1(x)) -> CHECK1(x)
Used argument filtering: CHECK1(x1) = x1
new1(x1) = x1
old1(x1) = old1(x1)
Used ordering: Precedence:
trivial
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
CHECK1(new1(x)) -> CHECK1(x)
The TRS R consists of the following rules:
top1(free1(x)) -> top1(check1(new1(x)))
new1(free1(x)) -> free1(new1(x))
old1(free1(x)) -> free1(old1(x))
new1(serve) -> free1(serve)
old1(serve) -> free1(serve)
check1(free1(x)) -> free1(check1(x))
check1(new1(x)) -> new1(check1(x))
check1(old1(x)) -> old1(check1(x))
check1(old1(x)) -> old1(x)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.
CHECK1(new1(x)) -> CHECK1(x)
Used argument filtering: CHECK1(x1) = x1
new1(x1) = new1(x1)
Used ordering: Precedence:
trivial
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ PisEmptyProof
↳ QDP
Q DP problem:
P is empty.
The TRS R consists of the following rules:
top1(free1(x)) -> top1(check1(new1(x)))
new1(free1(x)) -> free1(new1(x))
old1(free1(x)) -> free1(old1(x))
new1(serve) -> free1(serve)
old1(serve) -> free1(serve)
check1(free1(x)) -> free1(check1(x))
check1(new1(x)) -> new1(check1(x))
check1(old1(x)) -> old1(check1(x))
check1(old1(x)) -> old1(x)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
TOP1(free1(x)) -> TOP1(check1(new1(x)))
The TRS R consists of the following rules:
top1(free1(x)) -> top1(check1(new1(x)))
new1(free1(x)) -> free1(new1(x))
old1(free1(x)) -> free1(old1(x))
new1(serve) -> free1(serve)
old1(serve) -> free1(serve)
check1(free1(x)) -> free1(check1(x))
check1(new1(x)) -> new1(check1(x))
check1(old1(x)) -> old1(check1(x))
check1(old1(x)) -> old1(x)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.